First UIP
求め方
方針
導出のレベルを考える
決定は0，そこから導出されるごとに1,2,……と増やしていく
変数ごとにこの値を管理する
導出レベル(ilevel)は単位節伝播を辿っていく戦略によって割り当てが変わりうるが，どのように割り当ててもImplication Graphの各点の導出レベルよりその点に入っていく点の導出レベルは小さく，出ていく点の導出レベルは大きいという性質を持つ 便宜的に矛盾の導出レベルを最大とすると，矛盾から Implication Graph を導出レベルを優先度として探索していくと，First UIP に着いたとき初めてキューの中身が1つだけ(=First UIP)になる